FDL - Step of Proof: primrec

Step of Proof: primrec_add

11,40

Inference at * 2 1
Iof proof for Lemma primrec add:

1. T : Type
2. n :

3. 0 < n
4.

, b:T, c:({0..((n - 1)+m)

}

T).
4. primrec((n - 1)+m;b;c) = primrec(n - 1;primrec(m;b;c);

i,t. c(i+m,t))
5. m :

6. b : T
7. c : {0..(n+m)

}

T
8. primrec((n - 1)+m;b;c) = primrec(n - 1;primrec(m;b;c);

i,t. c(i+m,t))

primrec(n+m;b;c) = primrec(n;primrec(m;b;c);

i,t. c(i+m,t))

by ((((((MoveToConcl (-1))

CollapseTHEN (GenConcl primrec(m;b;c) = b'))

)

CollapseTHEN (

C(Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n)) (first_tok SupInf:t) inil_term)))

)

C(CollapseTHEN (Try ((ExtWith [`z'] [{0..(n+m)

}

T])

CollapseTHEN ((Auto_aux (first_nat 1:n

C) ((first_nat 2:n),(first_nat 3:n)) (first_tok SupInf:t) inil_term)))

))

C1:

C1: 8. b' : T

C1: 9. primrec(m;b;c) = b'

C1: 10. primrec((n - 1)+m;b;c) = primrec(n - 1;b';

i,t. c(i+m,t))

C1:

primrec(n+m;b;c) = primrec(n;b';

i,t. c(i+m,t))

Definitions P & Q, suptype(S; T), S T, , i j < k, t T, P Q, {i..j}, x:A. B(x), False, A, A B,

Lemmas le wf, int seg wf, primrec wf

Definitions	P & Q, suptype(S; T), S T, , i j < k, t T, P Q, {i..j}, x:A. B(x), False, A, A B,
Lemmas	le wf, int seg wf, primrec wf